/-
Copyright (c) 2025 Rémy Degenne. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rémy Degenne, Sébastien Gouëzel
-/
module

public import Mathlib.Topology.Order.Basic
public import Mathlib.Data.Fintype.WithTopBot

/-! # Order topology on `WithTop ι`

When `ι` is a topological space with the order topology, we also endow `WithTop ι` with the order
topology. If `ι` is second countable, we prove that `WithTop ι` also is.
-/

@[expose] public section

open Set Filter
open scoped Topology

namespace TopologicalSpace

variable {ι : Type*} [Preorder ι]

@[nolint unusedArguments]
instance [TopologicalSpace ι] [OrderTopology ι] : TopologicalSpace (WithTop ι) :=
  Preorder.topology _

instance [TopologicalSpace ι] [OrderTopology ι] : OrderTopology (WithTop ι) := ⟨rfl⟩

instance [ts : TopologicalSpace ι] [ht : OrderTopology ι] [SecondCountableTopology ι] :
    SecondCountableTopology (WithTop ι) := by
  classical
  rcases isEmpty_or_nonempty ι with hι | ⟨⟨x₀⟩⟩
  · infer_instance
  /- Let `c` be a countable set in `ι` such that the topology is generated by the sets `Iio a`
  and `Ioi a` for `a ∈ c`, by second-countability. Let `c'` be a dense set in `ι`, again by
  second-countability. Let `d` in `WithTop ι` be obtained from `c ∪ c'`, by adding `⊤` and a point
  `x₁ : ι` with `Ioi x₁ = ∅` if there is one.
  We will show that the topology on `WithTop ι` is generated by the intervals `Iio a` and `Ioi a`
  for `a ∈ d`, which will conclude the proof by countability of `d`. -/
  obtain ⟨c, c_count, hc⟩ : ∃ (c : Set ι), c.Countable ∧
      ts = generateFrom { s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a } :=
    exists_countable_generateFrom_Ioi_Iio ι
  obtain ⟨c', c'_count, hc'⟩ : ∃ c' : Set ι, c'.Countable ∧ Dense c' :=
    SeparableSpace.exists_countable_dense
  let x₁ : ι := if h : ∃ x, Ioi x = ∅ then h.choose else x₀
  let d : Set (WithTop ι) := (↑)'' c ∪ (↑)'' c' ∪ {⊤} ∪ {(x₁ : WithTop ι)}
  suffices H : instWithTopOfOrderTopology
      = generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a} by
    refine ⟨{s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}, ?_, by rw [← H]⟩
    have d_count : d.Countable :=
      (((c_count.image _).union (c'_count.image _)).union (by simp)).union (by simp)
    have : {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a} = Ioi '' d ∪ Iio '' d := by
      ext; simp; grind
    rw [this]
    exact (d_count.image _).union (d_count.image _)
  -- We should check the easy direction that all the elements in our generating set are open.
  -- This is trivial as these are all intervals.
  apply le_antisymm
  · apply le_generateFrom_iff_subset_isOpen.2
    simp only [setOf_subset_setOf, forall_exists_index, and_imp]
    grind [isOpen_Iio', isOpen_Ioi']
  /- Now, let us check that our sets indeed generates the topology. As the topology is
  generated by the open half-infinite intervals by definition, we should check that open
  half-infinite intervals are covered by finite intersections of our sets. -/
  let basis : Set (Set ι) := {s | ∃ (f g : Set ι), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite
      ∧ s = (⋂ a ∈ f, Ioi a) ∩ (⋂ a ∈ g, Iio a)}
  have h_basis : IsTopologicalBasis basis := isTopologicalBasis_biInter_Ioi_Iio_of_generateFrom c hc
  rw [OrderTopology.topology_eq_generate_intervals (α := WithTop ι)]
  apply le_generateFrom_iff_subset_isOpen.2
  simp only [setOf_subset_setOf, forall_exists_index]
  rintro u a (rfl | rfl)
  -- Consider an interval of the form `Ioi a`. We should cover it by finite intersections of
  -- our sets.
  · induction a with
    | top =>
      -- for `a = ⊤`, this is trivial as `Ioi ⊤` is in our set by design
      apply isOpen_generateFrom_of_mem
      exact ⟨⊤, by simp [d]⟩
    | coe a =>
      -- for `a : ι`, we consider an element `b ∈ Ioi a`, and seek a finite intersection of our
      -- sets containing it and contained in `Ioi a`.
      rw [@isOpen_iff_forall_mem_open]
      intro b hb
      induction b with
      | top =>
        -- if `b = ⊤`, then either `Ioi a` is empty in `ι` and then we use `Ioi (↑x₁)` which is
        -- in our set and reduced to `⊤`
        rcases eq_empty_or_nonempty (Ioi a) with ha | ha
        · refine ⟨Ioi x₁, ?_, ?_, by simp⟩
          · have : Ioi x₁ = ∅ := by
              have h : ∃ x, Ioi x = ∅ := ⟨a, ha⟩
              simp only [x₁, h, ↓reduceDIte]
              exact h.choose_spec
            simp [WithTop.Ioi_coe, this]
          · apply isOpen_generateFrom_of_mem
            simp [d]
        -- If `Ioi a` is not empty in `ι`, it contains a point `b` in the dense set `c'`, and then
        -- we use `Ioi (↑b)` which is in our set, contained in `Ioi (↑a)` and contains `⊤`.
        · obtain ⟨b, bc', hb⟩ : ∃ b ∈ c', b ∈ Ioi a := hc'.exists_mem_open (isOpen_Ioi' a) ha
          refine ⟨Ioi b, ?_, ?_, by simp⟩
          · apply Ioi_subset_Ioi
            simpa using hb.le
          · apply isOpen_generateFrom_of_mem
            exact ⟨b, by simp [d, bc'], Or.inl rfl⟩
      | coe b =>
        -- if `b` comes from `ι`, then in `ι` we can find a finite intersection of our sets
        -- containing `b` and contained in `Ioi a`. We lift it to `WithTop ι`.
        simp only [mem_Ioi, WithTop.coe_lt_coe] at hb
        obtain ⟨t, ⟨f, g, hfc, hgc, f_fin, g_fin, rfl⟩, hb, hfg⟩ :
          ∃ t ∈ basis, b ∈ t ∧ t ⊆ Ioi a := h_basis.isOpen_iff.1 (isOpen_Ioi' a) b hb
        refine ⟨(⋂ z ∈ f, Ioi z) ∩ ⋂ z ∈ g, Iio z, ?_, ?_, by simpa using hb⟩
        · intro w hw
          induction w with
          | top => simp
          | coe w =>
            simp only [mem_Ioi, WithTop.coe_lt_coe]
            apply hfg
            simpa using hw
        · apply @IsOpen.inter _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
          · apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
            · exact f_fin
            · intro i hi
              apply isOpen_generateFrom_of_mem
              grind
          · apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
            · exact g_fin
            · intro i hi
              apply isOpen_generateFrom_of_mem
              grind
  -- Consider an interval of the form `Iio a`. We should cover it by finite intersections of
  -- our sets.
  · induction a with
    | top =>
      -- for `a = ⊤`, this is trivial as `Iio ⊤` is in our set by design
      apply isOpen_generateFrom_of_mem
      exact ⟨⊤, by simp [d]⟩
    | coe a =>
      -- for `a : ι`, we consider an element `b ∈ Iio a`, and seek a finite intersection of our
      -- sets containing it and contained in `Iio a`.
      rw [@isOpen_iff_forall_mem_open]
      intro b hb
      induction b with
      | top => simp at hb
      | coe b =>
        -- `b` can not be equal to `⊤`, so it comes from `ι`. In `ι` we can find a finite
        -- intersection of our sets containing `b` and contained in `Iio a`. We lift it
        -- to `WithTop ι`, and intersect with `Iio ⊤` (which is also in our set) to exclude `⊤`.
        simp only [mem_Iio, WithTop.coe_lt_coe] at hb
        obtain ⟨t, ⟨f, g, hfc, hgc, f_fin, g_fin, rfl⟩, hb, hfg⟩ :
          ∃ t ∈ basis, b ∈ t ∧ t ⊆ Iio a := h_basis.isOpen_iff.1 (isOpen_Iio' a) b hb
        refine ⟨(⋂ z ∈ f, Ioi z) ∩ (⋂ z ∈ g, Iio z) ∩ Iio ⊤, ?_, ?_, by simpa using hb⟩
        · intro w hw
          induction w with
          | top => simp at hw
          | coe w =>
            simp only [mem_Iio, WithTop.coe_lt_coe]
            apply hfg
            simpa using hw
        · apply @IsOpen.inter _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}); swap
          · apply isOpen_generateFrom_of_mem
            simp [d]
          apply @IsOpen.inter _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
          · apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
            · exact f_fin
            · intro i hi
              apply isOpen_generateFrom_of_mem
              grind
          · apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
            · exact g_fin
            · intro i hi
              apply isOpen_generateFrom_of_mem
              grind

end TopologicalSpace

namespace WithTop

variable {ι : Type*} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι]

section Coe

lemma isEmbedding_coe : Topology.IsEmbedding ((↑) : ι → WithTop ι) := by
  refine WithTop.coe_strictMono.isEmbedding_of_ordConnected (α := ι) ?_
  rw [WithTop.range_coe]
  exact Set.ordConnected_Iio

lemma isOpenEmbedding_coe : Topology.IsOpenEmbedding ((↑) : ι → WithTop ι) :=
  ⟨isEmbedding_coe, by rw [WithTop.range_coe]; exact isOpen_Iio⟩

lemma nhds_coe {r : ι} : 𝓝 (r : WithTop ι) = (𝓝 r).map (↑) :=
  (isOpenEmbedding_coe.map_nhds_eq r).symm

@[fun_prop, continuity]
lemma continuous_coe : Continuous ((↑) : ι → WithTop ι) := isEmbedding_coe.continuous

end Coe

section ContinuousUnTop

lemma tendsto_untopD (d : ι) {a : WithTop ι} (ha : a ≠ ⊤) :
    Tendsto (untopD d) (𝓝 a) (𝓝 (untopD d a)) := by
  lift a to ι using ha
  rw [nhds_coe, tendsto_map'_iff]
  exact tendsto_id

lemma continuousOn_untopD (d : ι) : ContinuousOn (untopD d) { a : WithTop ι | a ≠ ⊤ } :=
  fun _a ha ↦ ContinuousAt.continuousWithinAt (tendsto_untopD d ha)

lemma tendsto_untopA [Nonempty ι] {a : WithTop ι} (ha : a ≠ ⊤) :
    Tendsto untopA (𝓝 a) (𝓝 a.untopA) := tendsto_untopD _ ha

lemma continuousOn_untopA [Nonempty ι] : ContinuousOn untopA { a : WithTop ι | a ≠ ⊤ } :=
  continuousOn_untopD _

lemma tendsto_untop (a : {a : WithTop ι | a ≠ ⊤}) :
    Tendsto (fun x ↦ untop x.1 x.2) (𝓝 a) (𝓝 (untop a.1 a.2)) := by
  have : Nonempty ι := ⟨untop a.1 a.2⟩
  simp only [← untopA_eq_untop, ne_eq, coe_setOf, mem_setOf_eq]
  exact (tendsto_untopA a.2).comp <| tendsto_subtype_rng.mp tendsto_id

lemma continuous_untop : Continuous (fun x : {a : WithTop ι | a ≠ ⊤} ↦ untop x.1 x.2) :=
  continuous_iff_continuousAt.mpr tendsto_untop

end ContinuousUnTop

variable (ι) in
/-- Homeomorphism between the non-top elements of `WithTop ι` and `ι`. -/
noncomputable
def neTopHomeomorph : { a : WithTop ι | a ≠ ⊤ } ≃ₜ ι where
  toEquiv := Equiv.withTopSubtypeNe
  continuous_toFun := continuous_untop
  continuous_invFun := continuous_coe.subtype_mk _

variable (ι) in
/-- If `ι` has a top element, then `WithTop ι` is homeomorphic to `ι ⊕ Unit`. -/
noncomputable
def sumHomeomorph [OrderTop ι] : WithTop ι ≃ₜ ι ⊕ Unit where
  toFun x := if h : x = ⊤ then Sum.inr () else Sum.inl x.untopA
  invFun x := match x with
    | Sum.inl i => (i : WithTop ι)
    | Sum.inr () => ⊤
  left_inv x := by cases x <;> simp
  right_inv x := by cases x <;> simp
  continuous_toFun := by
    have h_fr : frontier ({⊤} : Set (WithTop ι)) = ∅ := by
      simp only [frontier, Set.finite_singleton, Set.Finite.isClosed, IsClosed.closure_eq]
      suffices interior ({⊤} : Set (WithTop ι)) = {⊤} by simp [this]
      rw [interior_eq_iff_isOpen]
      have : {⊤} = Set.Ioi ((⊤ : ι) : WithTop ι) := by ext; simp
      rw [this]
      exact isOpen_Ioi
    refine continuous_if' (by simp [h_fr]) (by simp [h_fr]) (by simp) ?_
    exact Continuous.comp_continuousOn (by fun_prop) continuousOn_untopA
  continuous_invFun := continuous_sum_dom.mpr ⟨by fun_prop, by fun_prop⟩

end WithTop
